package tr.edu.ege.kipler.satisfiability.container.operational;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.FormulaBase;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class ModifiedIndividualObserver implements ABoxChangeObserver {

	public void afterFormulaIsAdded(FormulaBase fBase, Formula formula)
			throws UnsatisfiableException {
		if (formula instanceof ConceptAssertion) {
			ConceptAssertion ca = (ConceptAssertion) formula;
			ABox abox = (ABox) fBase;
			WcsData wcsData = abox.getWorld().getWcs().getData();
			wcsData.getModifiedIndividuals().add(abox.getWorld().getName(),
					ca.getName());
		}

	}

	public void afterNodeIsRemoved(FormulaBase fBase, Individual indv) {
		// Nothing to do
	}

}
